!pip  -q install --upgrade pyprover9
import pyprover9

ASSUMPTIONS = """

    % SORT AXIOMS: Establish two sorts.
    all x (Entity(x) | World(x)).
    all x -(Entity(x) & World(x)).
    all w all v (A(w,v) -> World(w) & World(v)).
    all a all w (In(a,w) -> Entity(a) & World(w)).

    % AXIOM B: Symmetry of the Accessibility relation.
    all w all v (World(w) & World(v) & A(w,v) -> A(v,w)).

    % AXIOM (alpha): No world is accessible from an empty world.
    all w all v ((World(w) & World(v) & (all a (Entity(a) -> -In(a,w))) & (exists b (Entity(b) & In(b,v)))) -> -A(w,v)).

    % AXIOM (beta): The F relation is well-founded.
    exists a (Entity(a) & all b all w all v ((Entity(b) & World(w) & World(v)) -> (-In(a,v) | -A(w,v) | -In(b,w) | In(a,w)))).

    % AXIOM (gamma): Every entity exists in some world.
    all a (Entity(a) -> exists w (World(w) & In(a,w))).

    % AXIOM (delta): For every contingent entity, a world where it does exists accesses to a world where it does not exist.
    all a ((Entity(a) & (exists w exists v (World(w) & World(v) & In(a,w) & -In(a,v)))) -> (exists u exists t (World(u) & World(t) & In(a,u) & -In(a,t) & A(u,t)))).
    
"""

GOAL = """
    % CONCLUSION (C): At least one necessary entity exists.
    exists a (Entity(a) & all w (World(w) -> In(a,w))).
"""

pyprover9.prove( ASSUMPTIONS, GOAL)